package model;

import java.util.Collection;
import java.util.Vector;

public class System {
	
	private final Net net;
	private Marking startMarking;
	
	public Marking getStartMarking() {
		return startMarking;
	}

	private void setMarking(final Marking marking) {
		this.startMarking = marking;
	}

	/**
	 * Constructor of System.
	 * @param net is the {@link Net} this {@link System} is based on.
	 * @param marking is the start {@link Marking}.
	 */
	public System(final Net net, final Marking marking) {
		this.net = net;
		this.startMarking = marking;
	}

	/**
	 * Executes all {@link Transition}s in the provided {@link Collection}.
	 * @param transitions are the {@link Transition} that are executed.
	 * @throws NotActivatedException if at least on {@link Transition} in this collection is not activated.
	 */
	public void execute(final Collection<Transition> transitions) throws NotActivatedException{
		this.setMarking(this.getPostExecutionMarking(this.startMarking, transitions));
	}
	
	/**
	 * Provides the {@link Marking} after the execution of all provided {@link Transition}s.
	 * @param transitions are the {@link Transition} that are executed.
	 * @throws NotActivatedException if at least on {@link Transition} in this collection is not activated.
	 */
	public Marking getPostExecutionMarking(final Marking marking, final Collection<Transition> transitions) throws NotActivatedException{
		if(!this.isActivated(marking, transitions)) throw new NotActivatedException();
		final Marking preProduct = this.net.getPre().multiply(transitions);
		final Marking postProduct = this.net.getPost().multiply(transitions);
		return Marking.add(Marking.subtract(marking, preProduct), postProduct);
	}
	
	private Marking getPostExecutionMarking(final Marking marking, final Transition transition) throws NotActivatedException {
		final Vector<Transition> transitions = new Vector<Transition>();
		transitions.add(transition);
		return this.getPostExecutionMarking(marking, transitions);
	}
	
	/**
	 * Provides true if all {@link Transition}s in the provided {@link Collection} can be executed
	 * @param transitions is a {@link Collection} of {@link Transition}.
	 * @return true if all {@link Transition}s can be executed. Else false.
	 */
	public boolean isActivated(final Marking marking, final Collection<Transition> transitions){
		final ArcMatrix preMatrix = this.net.getPre();
		final Marking requiredMarking = preMatrix.multiply(transitions);
		final Marking result = Marking.subtract(marking,requiredMarking);
		return result.greaterEqualZeroVector();
	}
	
	/**
	 * Provides true if there are finite reachable markings in this {@link System}.
	 * @return true if there are finite reachable markings in this {@link System}.
	 */
	public boolean hasFiniteReachableMarkings() {
		final StartMarkingTreeElement startMarkingTreeElement = new StartMarkingTreeElement(this.startMarking);
		final Vector<Marking> knownMarkings = new Vector<Marking>();
		knownMarkings.add(this.startMarking);
		return this.hasFiniteReachableMarkings(this.startMarking, startMarkingTreeElement, knownMarkings);
	}
	
	/**
	 * Provides true if no {@link Marking}s can be reached from the startMarking or when all {@link Marking}s than can be reached from the 
	 * startMarking are not in the provided marking tree. Else false.
	 * @param startMarking is the start {@link Marking}.
	 * @param markingTreeElement is the {@link Marking} tree.
	 * @param knownMarkings are all {@link Marking}s that are known.
	 */
	private boolean hasFiniteReachableMarkings(final Marking startMarking, final MarkingTreeElement markingTreeElement, final Vector<Marking> knownMarkings) {
		for (final Marking marking : this.getReachableMarkings(startMarking)) {
			if(!knownMarkings.contains(marking)){
				if(markingTreeElement.containsSubmarkingOf(marking)){
					return false;
				}
				knownMarkings.add(marking);
				if(!this.hasFiniteReachableMarkings(marking, new CompositeMarkingTreeElement(marking, markingTreeElement), knownMarkings)){
					return false;
				}
			}
		}
		return true;
	}


	/**
	 * Provides true if all possible {@link Marking}s but the initial {@link Marking} in this {@link System} can
	 * reach the initial {@link Marking} with all their possible {@link Transition}s.
	 */
	public boolean isCyclic(){
		final StartMarkingTreeElement startMarkingTreeElement = new StartMarkingTreeElement(this.startMarking);
		final Vector<Marking> knownMarkings = new Vector<Marking>();
		knownMarkings.add(this.startMarking);
		return this.isCyclic(this.startMarking, startMarkingTreeElement, knownMarkings);
	}

	/**
	 * Provides false when no markings can be reached or when a reachable {@link Marking} is in the provided marking tree.
	 * Else fasle.
	 * @param startMarking is the start {@link Marking}.
	 * @param markingTreeElement is the marking tree.
	 * @param knownMarkings are all known {@link Marking}s.
	 */
	private boolean isCyclic(final Marking startMarking,
							 final MarkingTreeElement markingTreeElement,
							 final Vector<Marking> knownMarkings) {
		final Collection<Marking> reachableMarkings = this.getReachableMarkings(startMarking);
		if(reachableMarkings.isEmpty()){
			java.lang.System.out.println("Not cyclic. Reason: no activated transitions (Deadlock)");			
			return false;
		}
		for (final Marking marking : reachableMarkings) {
			if(knownMarkings.contains(marking)){
//				if(!marking.equals(markingTreeElement.getStartMarking())){
//					if(markingTreeElement.contains(marking)){
//						java.lang.System.out.println("Not cyclic. Reason: previous marking in this path reached (Livelock).");
//						return false;
//					}
//				}
			} else{
				knownMarkings.add(marking);
				if(!this.isCyclic(marking, new CompositeMarkingTreeElement(marking, markingTreeElement),knownMarkings)){
					return false;
				}
			}
		}
		return true;
	}
	
	/**
	 * Provides all {@link Marking} that can be reached with a single {@link Transition} from the provided start {@link Marking}.
	 * @param startMarking is the start {@link Marking}.
	 */
	private Collection<Marking> getReachableMarkings(final Marking startMarking) {
		final Collection<Marking> result = new Vector<Marking>();
		for (final Transition transition : this.net.getTransitions()) {
			try {
				result.add(this.getPostExecutionMarking(startMarking, transition));
			} catch (final NotActivatedException e) {}
		}
		return result;
	}
	
	/**
	 * Provides true if all {@link Transition}s in the order provided in the {@link ExecutionSequence} are activated.
	 * @param sequence is the {@link ExecutionSequence} which is tested.
	 */
	public boolean isRealizable(final ExecutionSequence sequence){
		return sequence.isRealizable(this, this.getStartMarking());
	}
}